$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, $s$:timedState(${\it ds}$). read{-}state($s$) $\in$ State(${\it ds}$)